1. Technical Field
The present invention relates to computer program verification and more particularly to systems and methods for analyzing a loop in a program.
2. Description of the Related Art
Many static analysis and verification techniques do not perform well on loops in programs, either due to loss of precision or due to state space explosion. Many attempts have been made to address this problem. These attempts include a guided static analysis approach. This approach uses an abstract interpretation along loop paths to discover a refined control flow structure of a loop as a means of improving the precision of the final solution of the abstract interpretation itself.
A variance analysis approach uses the control flow of the loops to discover a set of ranking functions to prove termination of programs. These approaches, while providing some improvements, do not protect against state space explosion or provide the needed precision to sufficiently analyze loops.